<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
<html>
<head>
<!--

  @(#)prover.html

-->
</head>
<body bgcolor="white">

实现定理证明器接口.

<h2>Package Specification</h2>

<pre>
prover类调用了定理证明器Vampyre进行蕴含证明，调用了Foci进行插值计算。
</pre>

<!--
<ul>
  <li><a href="">##### REFER TO ANY FRAMEMAKER SPECIFICATION HERE #####</a>
</ul>
-->

<h2>Related Documentation</h2>

有关prover设计的其他资料：
<ul>
  <li><a href="./doc-files/prover.jpg">prover类图</a>
</ul>
有关定理证明器的资料：
<ul>
  <li><a href="http://www.cs.ucla.edu/˜rupak/Vampyre/">Vampyre下载</a>
  <li><a href="http://www.kenmcmil.com/foci.html">Foci下载</a>
</ul>

<!-- Put @see and @since tags down here. -->

</body>
</html>
